Inference at * 
Iof proof for Lemma before last:


  T:Type, L:(T List), x:T. (x  L)  ((x = last(L)))  x before last(L)  L 

latex

 by InductionOnList 

latex

 1: 

 1: 1. T : Type
 1: 2. T List
 1:   x:T. (x  [])  ((x = last([])))  x before last([])  []
 2: 

 2: 1. T : Type
 2: 2. T List
 2: 3. u : T
 2: 4. v : T List
 2: 5. x:T. (x  v)  ((x = last(v)))  x before last(v)  v
 2:   x:T. (x  [u / v])  ((x = last([u / v])))  x before last([u / v])  [u / v]
 .

Definitions	t  T, x:A. B(x)
Lemmas	l before wf, not wf, l member wf